$\forall$${\it es}$:ES, ${\it ff}$:FIFO, $p$:(E$\rightarrow\mathbb{P}$), $i$, $j$:${\it ff}$.C, $e$:E.
\\[0ex]($\forall$$i$:${\it ff}$.C, $e$:E. Dec(${\it ff}$.R($i$,$e$))) $\Rightarrow$ [$e$: $i$ $--$$p$$\rightarrow$ $j$] $\Rightarrow$ [${\it ff}$.Receiver($i$,$j$,$e$): $j$ $\leftarrow$$p$$--$ $i$]